(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(declare-fun d () String)
(declare-fun e () String)
(assert (= b "\x20\x2d\x20\x3c\x61\x20\x68\x72\x65\x66\x3d\x5c\x22\x6d\x6f\x64\x5f\x70\x6c\x75\x67\x69\x6e\x73\x2e\x70\x68\x70\x3f\x61\x63\x74\x69\x6f\x6e\x3d\x69\x6e\x73\x74\x61\x6c\x6c\x26\x70\x6c\x75\x67\x69\x6e\x5f\x66\x69\x6c\x65\x3d"))
(assert (= c (str.++ a b)))
(assert (distinct d "\x22\x3e\x49\x6e\x73\x74\x61\x6c\x6c\x3c\x2f\x61\x3e\x20\x5c\x6e"))
(assert (= e (str.++ c d)))
(assert (str.in_re e (re.++ (re.opt re.allchar) (str.to_re "\x5c\x3c\x53\x43\x52\x49\x50\x54") (re.opt re.all))))
(check-sat)
